ds:Top. update-spec-decl(;ds) 

latex

Definitions	Id, t  T, type List, nil, x:A. B(x), (x  l), b, P  Q, update-spec-vars(upd), update-spec-decl(upd;ds), Top, , False, x:AB(x), x:AB(x), P & Q, P  Q, {T}
Lemmas	nil member, top wf, l member wf, Id wf